i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da).
((fpf-dom(id-deq; mkid{ecl:ut2}; ds)))
 (ecl-machine1{ecl:ut2}(i; ds; da; A)  es_realizer{i:l}) 

latex

Definitions	Id, spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), P  Q, x:A. B(x), mkid{$x:ut2}, x. t(x), t  T, ecl-machine1{$ecl:ut2}(i; ds; da; A), x(s), ecl-trans-tuple{i:l}(ds; da), prop{i:l}
Lemmas	fpf-trivial-subtype-top, fpf-dom wf, fpf-compatible-single, ecl-trans-tuple wf, id-deq wf, assert wf, Knd wf, R-state-var-init wf, Id wf, fpf wf, ecl wf, ecl-trans wf, not wf